[Lucas - JFLP'98, Example 15]

Example 15 in [Lucas - JFLP'98]

Summary: Ex15_Luc98

CS-TRS Ex15_Luc98 (file Ex15_Luc98.csr)

Functions:  and true false if add 0 s first nil cons from

Constructors:  true false 0 s nil cons

Variables:  X Y Z

Arities: 

ar(and) = 2
ar(true) = 0
ar(false) = 0
ar(if) = 3
ar(add) = 2
ar(0) = 0
ar(s) = 1
ar(first) = 2
ar(nil) = 0
ar(cons) = 2
ar(from) = 1

Replacement map: 

µ(and)={1}
µ(true)={}
µ(false)={}
µ(if)={1}
µ(add)={1}
µ(0)={}
µ(s)={}
µ(first)={1,2}
µ(nil)={}
µ(cons)={}
µ(from)={}

Rules:  (file Ex15_Luc98)  

and(true,X) -> X
and(false,Y) -> false
if(true,X,Y) -> X
if(false,X,Y) -> Y
add(0,X) -> X
add(s(X),Y) -> s(add(X,Y))
first(0,X) -> nil
first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
from(X) -> cons(X,from(s(X)))

The CS-TRS in OBJ format (file Ex15_Luc98.obj):

obj Ex15_Luc98 is
  sort S .
  op and : S S -> S [strat (1 0)] .
  op true : -> S .
  op false : -> S .
  op if : S S S -> S [strat (1 0)] .
  op add : S S -> S [strat (1 0)] .
  op 0 : -> S .
  op s : S -> S [strat (0)] .
  op first : S S -> S .
  op nil : -> S .
  op cons : S S -> S [strat (0)] .
  op from : S -> S [strat (0)] .
  vars X Y Z : S .
  eq and(true,X) = X .
  eq and(false,Y) = false .
  eq if(true,X,Y) = X .
  eq if(false,X,Y) = Y .
  eq add(0,X) = X .
  eq add(s(X),Y) = s(add(X,Y)) .
  eq first(0,X) = nil .
  eq first(s(X),cons(Y,Z)) = cons(Y,first(X,Z)) .
  eq from(X) = cons(X,from(s(X))) .
endo

Negative results

  1. The µ-termination of Ex15_Luc98 cannot be proved by using Lucas' transformation. The TRS Ex15_Luc98_L: 
        and(true) -> X
    and(false) -> false
    if(true) -> X
    if(false) -> Y
    add(0) -> X
    add(s) -> s
    first(0) -> nil
    first(s,cons) -> cons
    from -> cons
    contains extra variables.

Positive results

  1. The µ-termination of Ex15_Luc98 can also be proved by using Giesl and Middeldorp's transformation: the TRS Ex15_Luc98_GM: 
        a__and(true,X) -> mark(X)
    a__and(false,Y) -> false
    a__if(true,X,Y) -> mark(X)
    a__if(false,X,Y) -> mark(Y)
    a__add(0,X) -> mark(X)
    a__add(s(X),Y) -> s(add(X,Y))
    a__first(0,X) -> nil
    a__first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
    a__from(X) -> cons(X,from(s(X)))
    mark(and(X1,X2)) -> a__and(mark(X1),X2)
    mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
    mark(add(X1,X2)) -> a__add(mark(X1),X2)
    mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
    mark(from(X)) -> a__from(X)
    mark(true) -> true
    mark(false) -> false
    mark(0) -> 0
    mark(s(X)) -> s(X)
    mark(nil) -> nil
    mark(cons(X1,X2)) -> cons(X1,X2)
    a__and(X1,X2) -> and(X1,X2)
    a__if(X1,X2,X3) -> if(X1,X2,X3)
    a__add(X1,X2) -> add(X1,X2)
    a__first(X1,X2) -> first(X1,X2)
    a__from(X) -> from(X)
    can be proved terminating (use MuTerm)
  2. The µ-termination of Ex15_Luc98 can also be proved by using Zantema's transformation: the TRS Ex15_Luc98_Z: 
    and(true,X) -> activate(X)
and(false,Y) -> false
if(true,X,Y) -> activate(X)
if(false,X,Y) -> activate(Y)
add(0,X) -> activate(X)
add(s(X),Y) -> s(n__add(activate(X),activate(Y)))
first(0,X) -> nil
first(s(X),cons(Y,Z)) -> cons(activate(Y),n__first(activate(X),activate(Z)))
from(X) -> cons(activate(X),n__from(n__s(activate(X))))
add(X1,X2) -> n__add(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> n__from(X)
s(X) -> n__s(X)
activate(n__add(X1,X2)) -> add(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__s(X)) -> s(X)
activate(X) -> X
    can be proved terminating (use AProVE)
  3. The µ-termination of Ex15_Luc98 can also be proved by using a polynomial interpretation (computed by MuTerm): 
        Proof of termination for CS-TRS  Ex15_Luc98:

    [and](X1,X2) = X1 + X2 + 1
    [true] = 0
    [false] = 0
    [if](X1,X2,X3) = X1 + X2 + X3 + 1
    [add](X1,X2) = 2.X1 + X2
    [0] = 1
    [s](X) = 1
    [first](X1,X2) = X1 + X2
    [nil] = 0
    [cons](X1,X2) = 0
    [from](X) = 1
  4. The µ-termination of Ex15_Luc98 can also be proved by using CSRPO (proof due to Albert Rubio):
    • marking map: 
          m(cons,2)=from
    • precedence: 
         add > s
   first > nil, cons, from
   from > cons, from', s
    • status: 
         st(first)=lex
    and automatically computed by MuTerm.
  5. The µ-termination of Ex15_Luc98 can also be proved by using CSDP (computed by MuTerm).